|
In mathematics, an idempotent binary relation ''R'' ⊆ ''X'' × ''X'' is one for which ''R'' ∘ ''R'' = ''R''.〔 Here:p.3〕 This notion generalizes that of an idempotent function to relations. Each idempotent relation is necessarily transitive, as the latter means ''R'' ∘ ''R'' ⊆ ''R''. For example, the relation < on ℚ is idempotent. In contrast, < on ℤ is not, since (<) ∘ (<) ⊇ (<) does not hold: e.g. 1 < 2, but 1 < ''x'' < 2 is false for every ''x'' ∈ ℤ. Idempotent relations have been used as an example to illustrate the application of Mechanized Formalisation of mathematics using the interactive theorem prover Isabelle/HOL. Besides checking the mathematical properties of finite idempotent relations, an algorithm for counting the number of idempotent relations has been derived in Isabelle/HOL. ==References== * 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Idempotent relation」の詳細全文を読む スポンサード リンク
|